Let Declarations

  let x = e;

In Cyclone, you can write as a local declaration. The meaning is the same as t x = e; where t is the type of e. In other words, x is bound to the new variable. Patterns are much more powerful because they can bind several variables to different parts of an aggregate object. Here is an example:

  struct Pair {  int x; int y; };
  void f(struct Pair pr) {
    let Pair(fst,snd) = pr;
    ...
  }

The pattern has the same structure as a struct Pair with parts being variables. Hence the pattern is a match for pr and the variables are initialized with the appropriate parts of pr. Hence “let Pair(fst,snd) = pr” is equivalent to “int fst =pr.x; int snd = pr.y”. A let-declaration’s initializer is evaluated only once.

Patterns may be as structured as the expressions against which they match. For example, given type

  struct Quad { struct Pair p1; struct Pair p2; };

patterns for matching against an expression of type struct Quad could be any of the following (and many more because of constants and wildcards–see below):

In general, a let-declaration has the form “let p = e;” where p is a pattern and e is an expression. In our example, the match always succeeds, but in general patterns can have compile-time errors or run-time errors.

At compile-time, the type-checker ensures that the pattern makes sense for the expression. For example, it rejects “let Pair(fst,snd) = 0” because 0 has type int but the pattern only makes sense for type struct Pair.

Certain patterns are type-correct, but they may not match run-time values. For example, constants can appear in patterns, so “let Pair(17,snd) = pr;” would match only when pr.x is 17. Otherwise the exception Match_Exception is thrown. Patterns that may fail are rarely useful and poor style in let-declarations; the compiler emits a warning when you use them. In switch statements, possibly-failing patterns are the norm—as we explain in Switch Statements, the whole point is that one of the cases’ patterns should match.